<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="tutorial.css">
<TITLE>
Execution Scheme
</TITLE>
</HEAD>
<BODY >
<A HREF="tutorial016.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial012.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial018.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc36">3.5</A>&nbsp;&nbsp;Execution Scheme</H2><UL>
<LI><A HREF="tutorial017.html#toc21">Resolution</A>
</UL>

<A NAME="toc21"></A>
<H3 CLASS="subsection"><A NAME="htoc37">3.5.1</A>&nbsp;&nbsp;Resolution</H3>
<A NAME="@default66"></A>
<A NAME="@default67"></A> <A NAME="@default68"></A>
Resolution is the computation rule used by Prolog. Given a set of
facts and rules as a program, execution begins with a query, which is
an initial goal that is to be resolved.
The set of goals that still have to be resolved is called the
<EM>resolvent</EM>.<BR>
<BR>
Consider again the <TT>ancestor/2</TT>
and <TT>parent/2</TT> predicate shown above.

	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#CCCCFF">
	<BLOCKQUOTE CLASS="quote"><PRE>
ancestor(X,Y) :- parent(X,Y).                 % clause 1
ancestor(X,Y) :- parent(Z,Y), ancestor(X,Z).  % clause 2 

parent(abe, homer).                           % clause 3
parent(abe, herbert).                         % clause 4
parent(homer, bart).                          % clause 5
parent(marge, bart).                          % clause 6
</PRE></BLOCKQUOTE></TD>
</TR></TABLE>
Program execution is started by issuing a query, for example
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
?- ancestor(X, bart).
</PRE></BLOCKQUOTE>
This is our initial resolvent.
The execution mechanism is now as follows:

	<BLOCKQUOTE CLASS="figure"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
	<BLOCKQUOTE CLASS="quote">
	
	
	
<OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
Pick one (usually the leftmost) goal from the resolvent.
 If the resolvent is empty, stop.
<LI CLASS="li-enumerate">Find all clauses whose head successfully unifies with this goal.
 If there is no such clause, go to step 6.
<LI CLASS="li-enumerate">Select the first of these clause. If there are more, remember the
 remaining ones. This is called a <EM>choice point</EM>.
<LI CLASS="li-enumerate">Unify the goal with the head of the selected clause.
 (this may instantiate variables both in the goal and in the clause's body).
<LI CLASS="li-enumerate">Prefix this clause body to the resolvent and go to 1.
<LI CLASS="li-enumerate"><A NAME="@default69"></A>
 Backtrack: Reset the whole computation state to
 how it was when the most recent choice point was created.
 Take the clauses remembered in this choice point and go to 3.
</OL>

	
	
	</BLOCKQUOTE>
	<BR>
<BR>
<DIV CLASS="center">Figure 3.3: Execution Algorithm</DIV><BR>
<BR>

	<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE>
In our example, the Prolog system would attempt to unify
<TT>ancestor(X, bart)</TT> with the program's
clause heads. Both clauses of the <TT>ancestor/2</TT> predicate can
unify with the goal, but the textually first clause, clause 1, is
selected first, and successfully unified with the goal:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
Goal (Query):   ancestor(X,bart)
Selected:       clause 1
Unifying:       ancestor(X,bart) = ancestor(X1,Y1)
results in:     X=X1, Y1=bart
New resolvent:  parent(X, bart)
More choices:   clause 2
</PRE></BLOCKQUOTE>
The body goal of clause 1 <CODE>parent(X, bart)</CODE> is added to the
resolvent, and the system remembers that there is an untried 
alternative &ndash; this is referred to as a <I>choice-point</I>.<BR>
<BR>
In the same way, <CODE>parent(X, bart)</CODE> is next selected for 
unification. Clauses 5 and 6 are possible matches for this goal,
with clause 5 selected first. There are no body goals to add, and
the resolvent is now empty:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
Goal:           parent(X, bart)
Selected:       clause 5
Unifying:       parent(X,bart) = parent(homer,bart)
results in:     X = homer
New resolvent:  
More choices:   clause 6, then clause 2
</PRE></BLOCKQUOTE>
The execution of a program completes successfully when there is an
empty resolvent. The program has thus found the first solution 
to the query, in the form of instantiations to the original Query's
variables, in this case <TT>X = homer</TT>. ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> returns this
solution, and also asks if we want more solutions:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
?- ancestor(X,bart).
X = homer     More? (;) 
</PRE></BLOCKQUOTE>
Responding with ';' will cause ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> to try to find alternative
solutions by <B>backtracking</B> to
the most recent choice-point, i.e. to seek an alternative to 
<TT>parent/2</TT>. Any bindings done during and after the selection of 
clause 5 are undone, i.e. the binding of X to <TT>homer</TT> is undone. Clause 6 is now unified with
the goal <TT>parent(X,Y)</TT>, which again produces a solution:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
Goal:           parent(X, bart)
Selected:       clause 6
Unifying:       parent(X,bart) = parent(marge,bart)
results in:     X = marge
New resolvent:  
More choices:   clause 2
</PRE></BLOCKQUOTE>
If yet further solutions are needed, then ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> would again backtrack.
This time, <TT>parent/2</TT> no longer has any alternatives left to unify,
so the next older choice-point, the one made for <TT>ancestor/2</TT>,
is the one that would be considered. The computation is returned
to the state it was in just before clause 1 was selected, and clause 2
is unified with the query goal:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
Goal:           ancestor(X,bart)
Selected:       clause 2
Unifying:       ancestor(X,bart) = ancestor(X1,Y1)
results in:     Y1 = bart, X1 = X
New resolvent:  parent(Z1, bart), ancestor(X1, Z1)
More choices:   
</PRE></BLOCKQUOTE>
For the first time, there are more than one goal in the resolvent, the
leftmost one, <TT>parent(Z1,bart)</TT> is then
selected for unification. Again, clauses 5 and 6 are candidates, and
a new choice-point is created, and clause 5 tried first.
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
Goal:           parent(Z1, bart)
Selected:       clause 5
Unifying:       parent(Z1, bart) = parent(homer, bart)
results in:     Z1 = homer
New resolvent:  ancestor(X1, homer)
More choices:   clause 6
</PRE></BLOCKQUOTE>
Eventually, after a few more steps
(via finding the ancestor of <TT>homer</TT>), this leads to a new solution, 
with <TT>abe</TT> returned as an ancestor of <TT>bart</TT>:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
?- ancestor(X,bart).
X = abe     More? (;) 
</PRE></BLOCKQUOTE>
If yet more solutions are requested, then because only one parent for
<TT>homer</TT> is given by the program, ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> would backtrack to the only 
remaining choice-point, unifying clause 6 is unified with the goal, 
binding <CODE>Z1</CODE> to <CODE>marge</CODE>. However, no ancestor for <TT>marge</TT>
can be found, because no parent of
<TT>marge</TT> is specified in the program. No more choice-points remains to
be tried, so the execution terminates.<BR>
<BR>
<HR>
<A HREF="tutorial016.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial012.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial018.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
